COMMENT ⊗   VALID 00005 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	(fasload met15)
C00013 00003	(setup)
C00021 00004	(Fasload met17)
C00022 00005	(Fasload met18)
C00024 ENDMK
C⊗;
(fasload met15)
(*rset (nouuo ()))

(setup)

(meter:report-frpoly)
Statistics
= <calls> (<percentage>)

Meter for: PCOEFADD
Cars = 98 (15.22%)
Signps = 94 (14.6%)
Atoms = 72 (11.18%)
Nulls = 66 (10.25%)
Conses = 54 (8.39%)
Cdrs = 48 (7.45%)
PCTIMES1 = 36 (5.59%)
PTIMES = 28 (4.35%)
PCTIMES = 28 (4.35%)
PCOEFADD = 26 (4.04%)
Zerops = 18 (2.8%)
PSIMP = 18 (2.8%)
Times's = 16 (2.48%)
Gets = 12 (1.86%)
PCPLUS = 12 (1.86%)
Putprops = 6 (0.93%)
Eqs = 6 (0.93%)
PPLUS = 6 (0.93%)
Oddps = 0 (0.0%)
Quotients = 0 (0.0%)
PEXPTSQ = 0 (0.0%)
Rplacds = 0 (0.0%)
<s = 0 (0.0%)
Rplacas = 0 (0.0%)
PTIMES3 = 0 (0.0%)
PTIMES2 = 0 (0.0%)
PTIMES1 = 0 (0.0%)
>s = 0 (0.0%)
=s = 0 (0.0%)
PPLUS1 = 0 (0.0%)
Pluses = 0 (0.0%)
Total = 644
T 
(meter:init-frpoly)
(bench 2)
(meter:report-frpoly)
Statistics
= <calls> (<percentage>)

Meter for: PCOEFADD
Signps = 381 (13.66%)
Cars = 369 (13.23%)
Cdrs = 324 (11.61%)
Nulls = 315 (11.29%)
Atoms = 300 (10.75%)
Conses = 180 (6.45%)
PTIMES = 123 (4.41%)
PCTIMES1 = 117 (4.19%)
PCOEFADD = 117 (4.19%)
PCTIMES = 114 (4.09%)
Times's = 78 (2.8%)
Zerops = 60 (2.15%)
PSIMP = 54 (1.94%)
Pluses = 36 (1.29%)
PTIMES2 = 27 (0.97%)
=s = 27 (0.97%)
PPLUS1 = 27 (0.97%)
PPLUS = 27 (0.97%)
>s = 18 (0.65%)
Eqs = 18 (0.65%)
PCPLUS = 18 (0.65%)
Rplacds = 9 (0.32%)
<s = 9 (0.32%)
Rplacas = 9 (0.32%)
PTIMES3 = 9 (0.32%)
PTIMES1 = 9 (0.32%)
Oddps = 6 (0.22%)
Quotients = 6 (0.22%)
PEXPTSQ = 3 (0.11%)
Putprops = 0 (0.0%)
Gets = 0 (0.0%)
Total = 2790
T 
(meter:init-frpoly)
(bench 5)
(meter:report-frpoly)
Statistics
= <calls> (<percentage>)

Meter for: PCOEFADD
Cars = 4413 (14.44%)
Cdrs = 4257 (13.93%)
Signps = 3516 (11.5%)
Nulls = 3501 (11.45%)
Atoms = 3294 (10.78%)
Conses = 1656 (5.42%)
PCOEFADD = 1110 (3.63%)
PTIMES = 1038 (3.4%)
PCTIMES = 942 (3.08%)
Times's = 768 (2.51%)
Pluses = 714 (2.34%)
PCTIMES1 = 624 (2.04%)
PPLUS = 609 (1.99%)
PPLUS1 = 555 (1.82%)
=s = 543 (1.78%)
PCPLUS = 465 (1.52%)
Zerops = 423 (1.38%)
PSIMP = 414 (1.35%)
>s = 366 (1.2%)
PTIMES2 = 345 (1.13%)
Eqs = 240 (0.79%)
<s = 198 (0.65%)
Rplacas = 198 (0.65%)
Rplacds = 132 (0.43%)
PTIMES3 = 132 (0.43%)
PTIMES1 = 96 (0.31%)
Oddps = 9 (0.03%)
Quotients = 9 (0.03%)
PEXPTSQ = 3 (0.01%)
Putprops = 0 (0.0%)
Gets = 0 (0.0%)
Total = 30570
T 
(meter:init-frpoly)
(bench 10)
(meter:report-frpoly)
Statistics
= <calls> (<percentage>)

Meter for: PCOEFADD
Cdrs = 50682 (15.05%)
Cars = 46686 (13.86%)
Atoms = 38700 (11.49%)
Signps = 37161 (11.03%)
Nulls = 36909 (10.96%)
Conses = 15285 (4.54%)
PCOEFADD = 10968 (3.26%)
PTIMES = 10641 (3.16%)
Pluses = 10239 (3.04%)
PCTIMES = 9864 (2.93%)
Times's = 9003 (2.67%)
PPLUS = 8709 (2.59%)
PCPLUS = 7485 (2.22%)
=s = 6708 (1.99%)
PPLUS1 = 6477 (1.92%)
>s = 5589 (1.66%)
PCTIMES1 = 3822 (1.13%)
PTIMES2 = 3531 (1.05%)
<s = 3456 (1.03%)
Rplacas = 3456 (1.03%)
Zerops = 2874 (0.85%)
PSIMP = 2862 (0.85%)
Eqs = 2001 (0.59%)
Rplacds = 1455 (0.43%)
PTIMES3 = 1455 (0.43%)
PTIMES1 = 777 (0.23%)
Oddps = 12 (0.0%)
Quotients = 12 (0.0%)
PEXPTSQ = 3 (0.0%)
Putprops = 0 (0.0%)
Gets = 0 (0.0%)
Total = 336822
T 
(meter:init-frpoly)
(bench 15)
(meter:report-frpoly)
Statistics
= <calls> (<percentage>)

Meter for: PCOEFADD
Cdrs = 384381 (16.78%)
Cars = 293511 (12.82%)
Atoms = 278784 (12.17%)
Signps = 247089 (10.79%)
Nulls = 242352 (10.58%)
Conses = 79140 (3.46%)
Pluses = 78024 (3.41%)
PTIMES = 71817 (3.14%)
PCTIMES = 67983 (2.97%)
PPLUS = 67575 (2.95%)
Times's = 65643 (2.87%)
PCPLUS = 62145 (2.71%)
PCOEFADD = 56466 (2.47%)
>s = 54225 (2.37%)
=s = 42726 (1.87%)
PPLUS1 = 37086 (1.62%)
<s = 35919 (1.57%)
Rplacas = 35919 (1.57%)
PTIMES2 = 19713 (0.86%)
Zerops = 11616 (0.51%)
PSIMP = 11604 (0.51%)
PCTIMES1 = 11271 (0.49%)
Rplacds = 11070 (0.48%)
PTIMES3 = 11070 (0.48%)
Eqs = 9264 (0.4%)
PTIMES1 = 3834 (0.17%)
Oddps = 12 (0.0%)
Quotients = 12 (0.0%)
PEXPTSQ = 3 (0.0%)
Putprops = 0 (0.0%)
Gets = 0 (0.0%)
Total = 2290254
T 
(fasload met16)
(*rset (nouuo ()))

(setup)
(meter:report-boyer)
Statistics
= <calls> (<percentage>)

Meter for: ADD-LEMMA
Cars = 424 (28.53%)
Atoms = 212 (14.27%)
Nulls = 107 (7.2%)
ADD-LEMMA-LST = 107 (7.2%)
Cdrs = 106 (7.13%)
Gets = 106 (7.13%)
Conses = 106 (7.13%)
Putprops = 106 (7.13%)
Eqs = 106 (7.13%)
ADD-LEMMA = 106 (7.13%)
TRUEP = 0 (0.0%)
Sub1s = 0 (0.0%)
TRANS-OF-IMPLIES1 = 0 (0.0%)
TRANS-OF-IMPLIES = 0 (0.0%)
TAUTP = 0 (0.0%)
TAUTOLOGYP = 0 (0.0%)
REWRITE-WITH-LEMMAS = 0 (0.0%)
REWRITE-ARGS = 0 (0.0%)
REWRITE = 0 (0.0%)
ONE-WAY-UNIFY1-LST = 0 (0.0%)
ONE-WAY-UNIFY1 = 0 (0.0%)
ONE-WAY-UNIFY = 0 (0.0%)
Members = 0 (0.0%)
Equals = 0 (0.0%)
FALSEP = 0 (0.0%)
APPLY-SUBST-LST = 0 (0.0%)
APPLY-SUBST = 0 (0.0%)
Total = 1486
T 
(meter:init-boyer)
(test)
(meter:report-boyer)
Statistics
= <calls> (<percentage>)

Meter for: ADD-LEMMA
Cars = 788408 (23.9%)
Cdrs = 462652 (14.03%)
Nulls = 434133 (13.16%)
Atoms = 419284 (12.71%)
Conses = 203872 (6.18%)
ONE-WAY-UNIFY1 = 171145 (5.19%)
REWRITE-ARGS = 169804 (5.15%)
REWRITE-WITH-LEMMAS = 152280 (4.62%)
Eqs = 128879 (3.91%)
ONE-WAY-UNIFY1-LST = 100601 (3.05%)
REWRITE = 91024 (2.76%)
Gets = 79742 (2.42%)
ONE-WAY-UNIFY = 73499 (2.23%)
APPLY-SUBST-LST = 11448 (0.35%)
APPLY-SUBST = 9512 (0.29%)
Equals = 1403 (0.04%)
Members = 272 (0.01%)
TRUEP = 207 (0.01%)
FALSEP = 150 (0.0%)
TAUTOLOGYP = 111 (0.0%)
TAUTP = 1 (0.0%)
Sub1s = 0 (0.0%)
TRANS-OF-IMPLIES1 = 0 (0.0%)
TRANS-OF-IMPLIES = 0 (0.0%)
ADD-LEMMA-LST = 0 (0.0%)
Putprops = 0 (0.0%)
ADD-LEMMA = 0 (0.0%)
Total = 3298427
T 
(setup)
(meter:report-boyer)
Statistics
= <calls> (<percentage>) [runtime (<percentage>)]

Meter for: ADD-LEMMA
Cars = 424 (28.53%) [7.0E-3 (19.44%)]
Atoms = 212 (14.27%) [2.0E-3 (5.56%)]
Nulls = 107 (7.2%) [0.0 (0.0%)]
ADD-LEMMA-LST = 107 (7.2%)
Cdrs = 106 (7.13%) [1.0E-3 (2.78%)]
Gets = 106 (7.13%) [2.0E-3 (5.56%)]
Conses = 106 (7.13%) [6.0E-3 (16.67%)]
Putprops = 106 (7.13%) [0.013 (36.11%)]
Eqs = 106 (7.13%) [5.0E-3 (13.89%)]
ADD-LEMMA = 106 (7.13%)
TRUEP = 0 (0.0%)
Sub1s = 0 (0.0%) [0.0 (0.0%)]
TRANS-OF-IMPLIES1 = 0 (0.0%)
TRANS-OF-IMPLIES = 0 (0.0%)
TAUTP = 0 (0.0%)
TAUTOLOGYP = 0 (0.0%)
REWRITE-WITH-LEMMAS = 0 (0.0%)
REWRITE-ARGS = 0 (0.0%)
REWRITE = 0 (0.0%)
ONE-WAY-UNIFY1-LST = 0 (0.0%)
ONE-WAY-UNIFY1 = 0 (0.0%)
ONE-WAY-UNIFY = 0 (0.0%)
Members = 0 (0.0%) [0.0 (0.0%)]
Equals = 0 (0.0%) [0.0 (0.0%)]
FALSEP = 0 (0.0%)
APPLY-SUBST-LST = 0 (0.0%)
APPLY-SUBST = 0 (0.0%)
Total = 1486	[0.036]
T 
(setq meter:sort-runtime t)
(meter:report-boyer)
Statistics
= <calls> (<percentage>) [runtime (<percentage>)]

Meter for: ADD-LEMMA
Putprops = 106 (7.13%) [0.013 (36.11%)]
Cars = 424 (28.53%) [7.0E-3 (19.44%)]
Conses = 106 (7.13%) [6.0E-3 (16.67%)]
Eqs = 106 (7.13%) [5.0E-3 (13.89%)]
Gets = 106 (7.13%) [2.0E-3 (5.56%)]
Atoms = 212 (14.27%) [2.0E-3 (5.56%)]
Cdrs = 106 (7.13%) [1.0E-3 (2.78%)]
TRUEP = 0 (0.0%)
Sub1s = 0 (0.0%) [0.0 (0.0%)]
TRANS-OF-IMPLIES1 = 0 (0.0%)
TRANS-OF-IMPLIES = 0 (0.0%)
TAUTP = 0 (0.0%)
TAUTOLOGYP = 0 (0.0%)
REWRITE-WITH-LEMMAS = 0 (0.0%)
REWRITE-ARGS = 0 (0.0%)
REWRITE = 0 (0.0%)
ONE-WAY-UNIFY1-LST = 0 (0.0%)
ONE-WAY-UNIFY1 = 0 (0.0%)
ONE-WAY-UNIFY = 0 (0.0%)
Members = 0 (0.0%) [0.0 (0.0%)]
Equals = 0 (0.0%) [0.0 (0.0%)]
FALSEP = 0 (0.0%)
APPLY-SUBST-LST = 0 (0.0%)
APPLY-SUBST = 0 (0.0%)
Nulls = 107 (7.2%) [0.0 (0.0%)]
ADD-LEMMA-LST = 107 (7.2%)
ADD-LEMMA = 106 (7.13%)
Total = 1486	[0.036]
T 
(setq meter:sort-runtime ())
NIL 
(meter:init-boyer)
(test)
(meter:report-boyer)
Statistics
= <calls> (<percentage>) [runtime (<percentage>)]

Meter for: ADD-LEMMA
Cars = 788408 (23.9%) [6.314 (0.09%)]
Cdrs = 462652 (14.03%) [3.733 (0.05%)]
Nulls = 434133 (13.16%) [3.543 (0.05%)]
Atoms = 419284 (12.71%) [4.087 (0.06%)]
Conses = 203872 (6.18%) [6824.346 (99.62%)]
ONE-WAY-UNIFY1 = 171145 (5.19%)
REWRITE-ARGS = 169804 (5.15%)
REWRITE-WITH-LEMMAS = 152280 (4.62%)
Eqs = 128879 (3.91%) [5.504 (0.08%)]
ONE-WAY-UNIFY1-LST = 100601 (3.05%)
REWRITE = 91024 (2.76%)
Gets = 79742 (2.42%) [2.674 (0.04%)]
ONE-WAY-UNIFY = 73499 (2.23%)
APPLY-SUBST-LST = 11448 (0.35%)
APPLY-SUBST = 9512 (0.29%)
Equals = 1403 (0.04%) [0.051 (0.0%)]
Members = 272 (0.01%) [0.024 (0.0%)]
TRUEP = 207 (0.01%)
FALSEP = 150 (0.0%)
TAUTOLOGYP = 111 (0.0%)
TAUTP = 1 (0.0%)
Sub1s = 0 (0.0%) [0.0 (0.0%)]
TRANS-OF-IMPLIES1 = 0 (0.0%)
TRANS-OF-IMPLIES = 0 (0.0%)
ADD-LEMMA-LST = 0 (0.0%)
Putprops = 0 (0.0%) [0.0 (0.0%)]
ADD-LEMMA = 0 (0.0%)
Total = 3298427	[6850.276]
T 
(setq meter:sort-runtime T)
(meter:report-boyer)
T 
Statistics
= <calls> (<percentage>) [runtime (<percentage>)]

Meter for: ADD-LEMMA
Conses = 203872 (6.18%) [6824.346 (99.62%)]
Cars = 788408 (23.9%) [6.314 (0.09%)]
Eqs = 128879 (3.91%) [5.504 (0.08%)]
Atoms = 419284 (12.71%) [4.087 (0.06%)]
Cdrs = 462652 (14.03%) [3.733 (0.05%)]
Nulls = 434133 (13.16%) [3.543 (0.05%)]
Gets = 79742 (2.42%) [2.674 (0.04%)]
Equals = 1403 (0.04%) [0.051 (0.0%)]
Members = 272 (0.01%) [0.024 (0.0%)]
TRUEP = 207 (0.01%)
Sub1s = 0 (0.0%) [0.0 (0.0%)]
TRANS-OF-IMPLIES1 = 0 (0.0%)
TRANS-OF-IMPLIES = 0 (0.0%)
TAUTP = 1 (0.0%)
TAUTOLOGYP = 111 (0.0%)
REWRITE-WITH-LEMMAS = 152280 (4.62%)
REWRITE-ARGS = 169804 (5.15%)
REWRITE = 91024 (2.76%)
ONE-WAY-UNIFY1-LST = 100601 (3.05%)
ONE-WAY-UNIFY1 = 171145 (5.19%)
ONE-WAY-UNIFY = 73499 (2.23%)
FALSEP = 150 (0.0%)
APPLY-SUBST-LST = 11448 (0.35%)
APPLY-SUBST = 9512 (0.29%)
ADD-LEMMA-LST = 0 (0.0%)
Putprops = 0 (0.0%) [0.0 (0.0%)]
ADD-LEMMA = 0 (0.0%)
Total = 3298427	[6850.276]
T 
(Fasload met17)
(*rset (nouuo ()))

(progn (setq test-pattern (init 6. 6. test-atoms)) t)
(meter:report-tprint)
Statistics
= <calls> (<percentage>)

Meter for: INIT
Conses = 2184 (23.82%)
<s = 1456 (15.88%)
Cdrs = 1133 (12.36%)
=s = 1093 (11.92%)
INIT1 = 1093 (11.92%)
1-s = 1092 (11.91%)
Cars = 1092 (11.91%)
Nulls = 21 (0.23%)
Rplacds = 1 (0.01%)
Substs = 1 (0.01%)
INIT = 1 (0.01%)
Total = 9167
T 
(Fasload met18)
(*rset (nouuo ()))

(progn (setq test-pattern (init 6. 6. test-atoms)) t)
(meter:report-fprint)
Statistics
= <calls> (<percentage>)

Meter for: INIT
Conses = 2184 (23.82%)
<s = 1456 (15.88%)
Cdrs = 1133 (12.36%)
=s = 1093 (11.92%)
INIT1 = 1093 (11.92%)
1-s = 1092 (11.91%)
Cars = 1092 (11.91%)
Nulls = 21 (0.23%)
Rplacds = 1 (0.01%)
Substs = 1 (0.01%)
INIT = 1 (0.01%)
Total = 9167
T